FDL - Nuprl Definition : pre-init-p

Nuprl Definition : pre-init-p

0,22

P holds in state init

e@i == (

v:T. P((

x.init(x)?

),v))

(

e:E. loc(e) = i)

clarification:

pre-init-p(es;i;ds;init;T;P)
== (

v:T. P((

x.fpf-cap(init;IdDeq;x;

)),v))

(

e:es-E(es). es-loc(es; e) = i

Id)

Definitions P Q, f(a), x.A(x), f(x)?z, IdDeq, , x:A. B(x), E, s = t, Id, loc(e)

FDL editor aliases pre-init-p

Definitions	P Q, f(a), x.A(x), f(x)?z, IdDeq, , x:A. B(x), E, s = t, Id, loc(e)
FDL editor aliases	pre-init-p